nLab Petri net

See also the Petri net in The Azimuth Project.

Introduction

Petri nets are a well known model of concurrent computation, generalising transition systems by using a built in notion of resource. Their use is widespread in modelling manufacturing systems, optimising control systems and in resource critical aspects of operational research, as well as being a useful model of computation. Because of this they exist in many variants : colored, algebraic, probabilistic, timed, …, and hence there are many forms of the basic definition, each thought best of that particular application.

The initial use, here, is for their links with transition systems, event structures, asynchronous automata etc., leading on to their comparison with higher dimensional automata? and higher dimensional transition systems, so the first definition we will use is that given by Winskel and Nielsen (see references below), but first we will attempt to give some idea of what a Petri net is and what it does.

Idea

The idea of a simple Petri net is based on a simple manufacturing shop. You have various ‘transitions’ or manufacturing ‘events’ that form part of the various process occurring in the ‘shop’. These typically take parts (of the final object), do something to them, such as combining two or more different parts to make a more complicated one, (for instance, putting the wheels on a car).

Parts, represented by ‘tokens’ are stored in ‘places’ and the assembly process are known, as above, as ‘events’ or ‘transitions’ (depending on the source being used for the theory). The relationships are typically represented graphically. For instance:

represents a system with three places (labelled $A$, $B$, and $C$) and one event/ transition (labelled $e$). Shown is a situation represented by an initial ‘marking’ where there are two tokens in $A$, one in $B$, and none in $C$. (The convention is that places are shown as circles and events as rectangles.)

Suppose that the ‘event’ takes one ‘part’ of type $A$, one of type $B$ and produces one of type $C$. (This is indicated on the diagram by the labels on the edges. Clearly with the available resources the even $e$ is able to be performed. (The usual Petri net jargon for this is that ‘$e$ is enabled’.) In this case, $e$ can be ‘fired’ and the result will yield a marking of one token in $A$, none in $B$ and one in $C$. This sort of structure gets abstracted as follows:

Definition

A Petri net $N$ consists of

• a set $P$ of places;

• an initial marking $M_0 \in \mathbb{N}^P$, so $M_0 : P \to \mathbb{N}$;

• a set $E$ of events; and

• two functions

  • $pre: P\times E\to \mathbb{N}$, and

  • $post: P\times E\to \mathbb{N}$.

Categorical Semantics of Petri Nets

The functions $pre$ and $post$ can be curried to write a Petri net as a pair of functions

where $\mathbb{N}[P]$ denotes the free commutative monoid on the set $P$ of places. Written this way, the analogy to graphs is clearer. The main difference is that now the source and target functions land in a free commutative monoid rather than just a set. Thus, Petri nets can be thought of as symmetric monoidal graphs because each edge is a multi-edge between a permutable sum of vertices. Just as graphs generate free categories, Petri nets should generate free symmetric monoidal categories. As Petri nets often model processes in various sciences, the free symmetric monoidal categories that they generate model the operational semantics of these processes. For a given Petri net $P$, the free symmetric monoidal category $FP$ that it generates should have objects given by possible markings of $P$, and morphisms given by ways of composing the events in sequence and in parallel.

The first to explore this idea were Meseguer and Montanari who constructed an adjunction between Petri nets and a subcategory of the category $CMC$ of commutative monoidal categories. This adjunction was modified in Petri nets based on Lawvere theories to get

Although morally Petri nets generate free symmetric monoidal categories, it turns out that because they have a free commutative monoid of places, they more naturally generate commutative monoidal categories, symmetric monoidal categories of an unusually strict type. Commutative monoidal categories don’t show up often in nature because they aren’t the result of a coherence theorem for symmetric monoidal categories. Mac Lane's coherence theorem for symmetric monoidal categories says that every symmetric monoidal category is symmetric monoidally equivalent to a strict symmetric monoidal category which may have nontrivial symmetry morphisms. However, commutative monoidal categories have symmetry morphisms which are given by the identity so they aren’t the strictifications of symmetric monoidal categories.

Computer scientists also haven’t been satisfied with commutative monoidal categories as a categorical semantics for Petri nets. Commutative monoidal categories are said to exhibit the collective token philosophy (see e.g. Glabeek and Plotkin), where tokens do not have individual identities. On the other hand, symmetric monoidal categories are said to have the individual token philosophy where the individual identities of the tokens are retained. The easiest to see where an issue shows up is with a variation of the Eckmann-Hilton argument. Let $C$ be a commutative monoidal category and let $f,g \colon a \to a$ be morphisms from an object a to itself. Then,

$$\begin{aligned} g \circ f + 1_a & = g \circ f + 1_a \circ 1_a \\ &= (g+ 1_a)\circ (f + 1_a) \\ &= (g + 1_a) \circ (1_a + f) \\ & = g \circ 1_a + 1_a \circ f \\ &= g + f \end{aligned}$$

So in a commutative monoidal category $g \circ f + 1_a = g+ f$ even though they have very different semantic interpretations: one represents sequential composition and the other represents parallel composition.

One possible fix to this is to change the definition of Petri net. In Functorial Models for Petri Nets the authors introduced pre-nets. A pre-net is a pair of functions from a set of events to the free monoid on a set of places. The key difference is that now every event is equipped with an ordering on the input and output of each transition. With pre-nets, there is a natural adjunction between the category $PreNet$ of pre-nets and $SMC$ the category of strict monoidal categories

which can be composed with the adjunction which freely adds symmetries to a strict monoidal category to get an adjunction

where $SSMC$ is the category of strict symmetric monoidal categories. This gives a categorical operational semantics for pre-nets which obeys the individual token philosophy and avoids the pitfall of the above computation. Pre-nets can be turned into Petri nets via abelianization. For a given Petri net $P$, its abelianization forgets about the ordering on the input and output of each event. Therefore, to obtain a categorical semantics for a Petri net $P$ which obeys the individual token philosophy, a pre-net $Q$ can be chosen which abelianizes to $P$. Then, the categorical semantics for $P$ can defined as the free strict symmetric monoidal category $L(Q)$.

References

• John Baez, Fabrizio Genovese, Jade Master, Michael Shulman, Categories of Nets, (arXiv:2101.04238)

• G. Winskel, M. Nielsen, Models for concurrency, Handbook of Logic in Computer Science vol. 3, pp. 100 – 200, Oxford Univ. Press 1994. (see also online technical report).

• John C. Baez and Jacob Biamonte, Quantum techniques in stochastic mechanics, World Scientific, 2018. World Scientific pdf

• wikipedia

For an introduction to Petri nets (en francais, which is very clear and accessible) look at

• Robert Valette?, Les Réseaux de Petri.

On the connection to linear logic:

• Uffe Engberg? and Glynn Winskel, Petri nets as models of linear logic. CAAP 1990. Lecture Notes in Computer Science, vol 431. Springer, Berlin, Heidelberg. Springer, pdf on ResearchGate

On the categorical semantics of Petri nets:

• José Meseguer and Ugo Montanari?, Petri nets are monoids, Information and Computation, Volume 88, Issue 2, Pages 105-155, 1990. journal, pdf

• Jade Master, Petri nets based on Lawvere theories, Mathematical Structures in Computer Science 30, no. 7 (2020): 833-864. Available at journal

• Roberto Bruni?, José Meseguer, Ugo Montanari?, and Vladimiro Sassone. Functorial models for Petri nets Information and Computation 170, no. 2 (2001): 207-236. pdf

• Rob J. van Glabbeek?, and Gordon Plotkin. Configuration structures, event structures and Petri nets Theoretical Computer Science 410, no. 41 (2009): 4111-4159. Available at pdf

category: computer science